<html>
<head><meta charset="utf-8"><title>Standards for verification tools · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html">Standards for verification tools</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="202496820"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202496820" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202496820">(Jun 30 2020 at 21:22)</a>:</h4>
<p>Reading <a href="https://alastairreid.github.io/rust-verification-tools/">https://alastairreid.github.io/rust-verification-tools/</a> bring up a topic I was considering when exploring this space; the lack of standards between different verification tools.</p>
<p>There are three different interfaces mentioned in this article for assertions and pre/post conditions (<a href="https://crates.io/crates/verifier">verifier</a>, Prusti's <a href="https://github.com/viperproject/rust-contracts">rust-contracts</a>, and <a href="https://gitlab.com/karroffel/contracts">contracts</a> used by MIRAI), plus <a href="https://github.com/nrc/libhoare">LibHoare</a> which wasn't mentioned in that list for some reason but was mentioned later (I suppose because it's only currently used for runtime checks and not static analysis, but it provides a similar contracts interface).</p>
<p>Additionally, in the fuzzing/property testing space, <a href="https://docs.rs/quickcheck/0.9.2/quickcheck/trait.Arbitrary.html">QuickCheck</a>, <a href="https://docs.rs/proptest/0.10.0/proptest/arbitrary/trait.Arbitrary.html">Proptest</a>, and <a href="https://github.com/rust-fuzz/arbitrary">rust-fuzz</a> each have their own <code>Arbitrary</code> trait.</p>
<p>It seems to me that it would be helpful to standardize on a bit more in this space, such as a generic contracts/properties language (subsettable and/or extensible so analyzer-specific extensions could be added), and an Arbitrary trait that could be shared by different engines. That could allow doing things like QuickCheck with contracts/properties as test-time assertions for easy, no dependency checking that might catch some quick and easy bugs, while you could use a full-fledged verifier that might have more dependencies (like Prusti, which depends on Java), or a full fledged fuzzer which might also have substantial dependencies, to get more in-depth analysis.</p>
<p>I've only just started exploring these tools, so I don't have a strong opinion of which Arbitrary trait has the best interface or what a core common contracts interface would look like, but I'm wondering if anyone has an opinion on which of the contracts crates or Arbitrary traits would be best as a starting point for standardization.</p>



<a name="202498542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202498542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202498542">(Jun 30 2020 at 21:38)</a>:</h4>
<p>On the Arbitrary side, <a href="https://docs.rs/proptest/0.10.0/proptest/strategy/trait.Strategy.html"><code>proptest::Strategy</code></a> seems more flexible, while it also provides <a href="https://docs.rs/proptest/0.10.0/proptest/arbitrary/trait.Arbitrary.html"><code>proptest::Arbitrary</code></a> which can be used for a quick default <code>Strategy</code> for a given type. But that's also more complex than <a href="https://docs.rs/quickcheck/0.9.2/quickcheck/trait.Arbitrary.html"><code>quickcheck::Arbitrary</code></a> or <a href="https://docs.rs/arbitrary/0.4.5/arbitrary/trait.Arbitrary.html"><code>arbitrary::Arbitrary</code></a>.</p>



<a name="202548648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202548648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202548648">(Jul 01 2020 at 09:38)</a>:</h4>
<p>hi Brian, I think this is a great idea. I don't know how much of a common subset there would be between different tools though. Proofs are going to be prover-aware since they'll need to use the underlying specification language / tools.</p>



<a name="202548686"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202548686" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202548686">(Jul 01 2020 at 09:39)</a>:</h4>
<p>it would be cool if there was a standard way for libs to declare (basic) contracts though, even if they don't verify them. That way users of provers wouldn't have to write wrappers to attach contracts.</p>



<a name="202549041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202549041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202549041">(Jul 01 2020 at 09:43)</a>:</h4>
<p>It would also be cool if provers could share a set of examples + specs to compare different tools since it's likely they each have different strengths/weaknesses.</p>
<p>On the other hand unifying the different <code>Arbitrary</code> classes seems more feasible. Do you know what they differ on?</p>



<a name="202573038"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202573038" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202573038">(Jul 01 2020 at 14:10)</a>:</h4>
<p>I suppose we could look at Eiffel / Ada contracts to see what language-level support for contracts could look like.</p>



<a name="202575584"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202575584" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202575584">(Jul 01 2020 at 14:31)</a>:</h4>
<p>Proptest and QuickCheck arbitrary impls differ in how they minify inputs, so they have somewhat different implementation requirements. There is a compatibility layer for the lazy, but I'm not sure if going from QuickCheck to proptest actually gets you the benefits of proptest. You can also get fuzzers to work with QuickCheck or proptest Arbitrary impls, but the results are worse than using fuzzing-aware Arbitrary directly.</p>



<a name="202575704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202575704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202575704">(Jul 01 2020 at 14:32)</a>:</h4>
<p>For reference, <a href="https://github.com/rust-secure-code/mem-markers">https://github.com/rust-secure-code/mem-markers</a> is an ongoing trait unification project among <code>zerocopy</code>, <code>bytemuck</code> and other crates that require certain invariants about data layout. Still in relatively early stages though.</p>



<a name="202599673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202599673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202599673">(Jul 01 2020 at 17:39)</a>:</h4>
<blockquote>
<p>it would be cool if there was a standard way for libs to declare (basic) contracts though, even if they don't verify them. That way users of provers wouldn't have to write wrappers to attach contracts.</p>
</blockquote>
<p>Yes, that's what I'm thinking of. Some kind of common core contracts system, so that libraries could declare various contract information, which could be used either as runtime assertions, maybe in some cases only in debug mode during testing or maybe sometimes at runtime, but which could also be used, potentially with some extra richer annotations for a given proof system, for formal verification.</p>



<a name="202601206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202601206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202601206">(Jul 01 2020 at 17:51)</a>:</h4>
<blockquote>
<p>Proptest and QuickCheck arbitrary impls differ in how they minify inputs, so they have somewhat different implementation requirements. There is a compatibility layer for the lazy, but I'm not sure if going from QuickCheck to proptest actually gets you the benefits of proptest. You can also get fuzzers to work with QuickCheck or proptest Arbitrary impls, but the results are worse than using fuzzing-aware Arbitrary directly.</p>
</blockquote>
<p>My main desire here would be to be able to more easily go from either QuickCheck or proptest to a fuzzer. QuickCheck or proptest are relatively simple to use without external tooling dependencies, and I think would be good for projects to be able to just have those as part of their normal test suite. They can be used for getting an <code>Arbitrary</code> implementation set up, and ensuring it still works as part of normal <code>cargo test</code>, and maybe catching some low-hanging issues, but they are likely to explore less of the relevant space than coverage guided fuzzers.</p>
<p>Then as part of your CI, you could set up a a coverage-guided fuzzer and let it run longer and explore the space more deeply given the coverage guided setup.</p>



<a name="202602165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202602165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202602165">(Jul 01 2020 at 18:00)</a>:</h4>
<blockquote>
<p>For reference, <a href="https://github.com/rust-secure-code/mem-markers">https://github.com/rust-secure-code/mem-markers</a> is an ongoing trait unification project among zerocopy, bytemuck and other crates that require certain invariants about data layout. Still in relatively early stages though.</p>
</blockquote>
<p>That's a good point, that without involving external verification tools, using the type system as a way of communicating and checking invariants has a lot of power, and some standard libraries of marker traits for such invariants could help out a lot.</p>



<a name="202664441"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202664441" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202664441">(Jul 02 2020 at 08:59)</a>:</h4>
<p>In Prusti we are exploring how to standardize the syntax of contracts such that different tools can then use them in different ways. One attempt is <a href="https://github.com/viperproject/rust-contracts">https://github.com/viperproject/rust-contracts</a>: contracts are procedural macros that by default do nothing. Tools can then <a href="https://github.com/viperproject/rust-contracts/blob/1dbee6f392cd6687905ae0d587b6c385bef578be/example_verification_tool/src/rustc.rs#L20-L29">replace the library used to execute the procedural macros</a> and do what they want with the contracts. Common parsing functionalities could be published on <a href="http://crates.io">crates.io</a> and shared between tools.</p>



<a name="202682529"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202682529" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202682529">(Jul 02 2020 at 12:47)</a>:</h4>
<blockquote>
<p>My main desire here would be to be able to more easily go from either QuickCheck or proptest to a fuzzer.</p>
</blockquote>
<p><a href="https://github.com/fitzgen/bufrng">https://github.com/fitzgen/bufrng</a> provides such a compatibility layer.</p>



<a name="202754888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202754888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202754888">(Jul 02 2020 at 23:20)</a>:</h4>
<blockquote>
<p><a href="https://github.com/fitzgen/bufrng">https://github.com/fitzgen/bufrng</a> provides such a compatibility layer.</p>
</blockquote>
<p>Ah, nice, I hadn't seen that. Thanks!</p>



<a name="202755059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202755059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202755059">(Jul 02 2020 at 23:24)</a>:</h4>
<p>fuzzers rely on the assumption that a small change in the input results in a small change in the control flow, not changes it completely. If that's not the case you're just running a random search and would be better off with an RNG. So if your <code>Arbitrary</code> impl performs a lot of input transformation (which depends on the types and complexity of your struct) fuzzers might not work particularly well</p>



<a name="202755175"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202755175" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Brian Campbell <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202755175">(Jul 02 2020 at 23:27)</a>:</h4>
<blockquote>
<p>One attempt is <a href="https://github.com/viperproject/rust-contracts">https://github.com/viperproject/rust-contracts</a>: contracts are procedural macros that by default do nothing.</p>
</blockquote>
<p>Yeah, it looks like <a href="https://gitlab.com/karroffel/contracts">https://gitlab.com/karroffel/contracts</a> is also supposed to be a library that can be used for standardized contracts as well; unfortunately, that means there's now two standards, one used by MIRAI and one by Prusti.</p>



<a name="202755266"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202755266" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202755266">(Jul 02 2020 at 23:29)</a>:</h4>
<p>Welp, <a href="https://xkcd.com/927/">https://xkcd.com/927/</a> was right.<br>
At least you have 2 competing standards and not 6 like safe transmute</p>



<a name="202774832"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202774832" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202774832">(Jul 03 2020 at 07:21)</a>:</h4>
<p><code>viperproject/rust-contracts</code> doesn't try to be a standard, it's not even on <a href="http://crates.io">crates.io</a>. It's an experiment to see whether a plugin-like architecture is feasible.</p>



<a name="202775376"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202775376" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202775376">(Jul 03 2020 at 07:30)</a>:</h4>
<p><code>karroffel/contracts</code> is really nice! However, the current design is monolithic, as it requires to implement tool-specific logic and syntax in the <code>contracts</code> crate. This inhibits the rapid development of new features, and I don't think that it's a scalable solution. Tools would have to wait for PRs to be discussed and merged, and the maintainer(s) of <code>contracts</code> would have to do tool-specific work.</p>



<a name="202778258"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202778258" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202778258">(Jul 03 2020 at 08:13)</a>:</h4>
<p>I sent an email to <code>karoffel</code> with a link to this stream; let's see if he can join.</p>



<a name="202918716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202918716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> karroffel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202918716">(Jul 05 2020 at 11:54)</a>:</h4>
<p>Hello! A bit late but I found my way <span aria-label="smile" class="emoji emoji-263a" role="img" title="smile">:smile:</span></p>



<a name="202918811"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202918811" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> karroffel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202918811">(Jul 05 2020 at 11:56)</a>:</h4>
<p>and yes, the <code>contracts</code> crate was originally made for dynamic checking, so that was all I coded it for in the beginning. I did talk about modularisation with MIRAI contributors, but since then no further development happened but it's not out of my vision :)</p>



<a name="202919312"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202919312" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> karroffel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202919312">(Jul 05 2020 at 12:13)</a>:</h4>
<p>I am thinking of adding something like a <code>#[contracts_provider]</code> attribute, similar to <code>#[global_allocator]</code>, that way the user crate could select the behaviour for the crate. That will be a bit tricky to get right in the general case as features like the <code>old()</code> pseudofunction need to capture variables and rewrite them in expressions. It might be possible but I'd have to think about that some more.<br>
My goal was to have a nice dynamic checking solution that works on stable and uses attributes. If a more flexible solution arises that fits my needs too then I have no issue advocating for that solution then, I am not heavily attached to the <code>contracts</code> crate</p>



<a name="202931952"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202931952" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202931952">(Jul 05 2020 at 18:15)</a>:</h4>
<p>Also see <a href="https://github.com/loiclec/fuzzcheck-rs">https://github.com/loiclec/fuzzcheck-rs</a></p>



<a name="202932118"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202932118" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202932118">(Jul 05 2020 at 18:19)</a>:</h4>
<p>Ohh that looks like a lovely project</p>



<a name="202932171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202932171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202932171">(Jul 05 2020 at 18:20)</a>:</h4>
<p>One to keep tabs on, at the very least</p>



<a name="202968466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/202968466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#202968466">(Jul 06 2020 at 09:23)</a>:</h4>
<blockquote>
<p>I am thinking of adding something like a <code>#[contracts_provider]</code> attribute, similar to <code>#[global_allocator]</code>, that way the user crate could select the behaviour for the crate.</p>
</blockquote>
<p>I just would like to point out that tools working on MIR like Prusti and MIRAI are implemented as Rustc drivers. This means that they (at least in theory) could replace the contracts crate with their custom version of it at runtime.</p>



<a name="203641786"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/203641786" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> karroffel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#203641786">(Jul 12 2020 at 12:31)</a>:</h4>
<p>That's true, that would be more interesting for dynamic checking. Custom rustc drivers can replace things like this on their own without a crate like <code>contracts</code> needing to do too much to support that (if I understood that correctly). But dynamic checking has a few other requirements too and depending on the situation might need different handling of the contracts.</p>



<a name="203641850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/203641850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> karroffel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#203641850">(Jul 12 2020 at 12:33)</a>:</h4>
<p>I don't think those two things are at odds, it would just allow people to add new ways of dealing with how contracts are handled at runtime more easily. For static checking the <code>#[contracts_provider]</code> could be a no-op for example.<br>
But it's just an idea I have been toying around with, I have no concrete implementation yet and it's all still blurry <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span></p>



<a name="203737580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Standards%20for%20verification%20tools/near/203737580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Standards.20for.20verification.20tools.html#203737580">(Jul 13 2020 at 16:33)</a>:</h4>
<blockquote>
<p>Custom rustc drivers can replace things like this on their own without a crate like contracts needing to do too much to support that (if I understood that correctly).</p>
</blockquote>
<p>As I learned the hard way, the drivers can replace the crate that is loaded, but they cannot do arbitrary AST rewriting. In other words, the rewriting that a driver can do is limited to capabilities of procedural macros.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>